$\forall$${\it es}$:ES, $A$, $B$:Type, $f$:($A$$\rightarrow$$B$), ${\it Ia}$:AbsInterface($A$). $f$'${\it Ia}$ $\in$ AbsInterface($B$)